Welcome
I am a CNRS researcher in the Love team at the LIPN. Here's a CV.
My research is motivated by the gap between the theory
programming languages and the applications of programming languages to
continuous mathematics. It lies at the interface of Logic, Formal Proofs
and Functional Analysis. I am a happy participant to the Math-Comp Analysis project.
Contact
News:
- I will be in the PC of MFCS 2025, ICFP 2025 and WoLLIC 2025.
- Mid-October, I've organized a two-day seminar for women and gender minorities at LIPN.
- Jad Koleilat will start his PhD thesis in October 2024, under my and Stefano Guerrini's supervision.
- Our paper ∂ is for Dialectica, with Pierre-Marie Pédrot , was a distinguished paper at LICS 2024.
- My ANR project DiPLo, focused on Logic and Differentiable
Programming, has been accepted. This will allow for the funding of a
two-years post-doc or two one-year ones in 2026 and 2027, and for the
organization of a workshop. News will be posted here, on Mastodon and on
the usual mailing lists!
- Our paper Laplace Distributors and Laplace Transformations for Differential Categories, with Jean-Simon Pacaud Lemay, was accepted to FSCD 2024.
- Our paper ∂ is for Dialectica, with Pierre-Marie Pédrot , was accepted to LICS 2024.
- With Adrien Guatto, I'll be co-chairing the JFLA 2025 conference.
Students and Interships
I am always happy to work with students, and have access to grants
for interns and PhD students. Please do not hesitate to contact me !
I'm also happy to supervise formalizations projets in Rocq.
Papers
Published articles
- Laplace Distributors and Laplace Transformations for Differential Categories, with Jean-Simon Pacaud Lemay, FSCD 2024. preprint .
- ∂ is for Dialectica, with Pierre-Marie Pédrot , LICS 2024. Distinguished paper, invited for a long version in Journal of the ACM. preprint .
- Unifying Graded Linear Logic and Differential Operators, with Simon Mirwasser and Flavien Breuvart, FSCD 2023. preprint. Selected for a special issue in LMCS, long version.
- Taylor Expansion as a Monad in Models of DiLL, with Jean-Simon Pacaud Lemay, LICS 2023. preprint .
- Utilisation des assistants de preuves pour l’enseignement en L1 with
Frédéric Le Roux, Patrick Massot, Micaela Mayero, Zoé Mesnil, Simon
Modeste, Julien Narboux, Pierre Rousselin, published in La gazette des
mathématiciens in 2022, preprint
- Competing inheritance paths in dependent type theory: a case study in functional analysis,
with Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling and
Kazuhiko Sakaguchi, accepted at IJCAR 2020 (conference). preprint
- Models of Linear Logic based on the Schwartz ε-product, with Yoann Dabrowski, 82 pages, 2020, published in Theory and Applications of Categories (journal). paper .
- Chiralités et exponentielles: un peu de différentiation, with Ésaïe Bauer, JFLA 2019 (national conference). preprint
- Higher-order distributions for Differential Linear Logic, with Jean-Simon Lemay, published at Fossacs 2019 (conference). preprint.
- A Logical Account for Linear Partial Differential Equations, 2018, LICS 2018 (conference). preprint
- Mackey-complete spaces and power series - A topological model of Differential Linear Logic, with Christine Tasson, 2018, Mathematical Structures in Computer Science (journal). preprint
- Weak topologies for Linear Logic, 2016, Logical Methods for Computer Science (journal). paper
Preprints
- Functorial models of DiLL, with Morgan Rogers and Valentin Maestracci, 2023. preprint .
- Chiralities in Topological Vector Spaces , 2019. preprint
Popularization
- A popularization article on formal proofs and semantics in Blog Binaire .
Thesis
- I defended my PhD thesis on October 19th 2018. You will find here the manuscript and the slides .
Teaching
- Logic for computer science (Université Sorbonne Paris Nord, L1, Lessons and exercice sessions, 2022-2023).
- Introduction to formal proofs (Université Sorbonne Paris Nord, L1,
joint lessons and exercice sessions, 2021-20222 and 2022-2023).
- Real analysis (Université Sorbonne Paris Nord, L2, Exercice sessions, 2021-20222).
Talks
General introductory talks
- An introduction to Differential Linear Logic, Invited talk at the "Differential λ-Calculus and Differential Linear Logic, 20 Years Later " conference, 2024.
- An introduction to ssreflect tactics , Invited talk at the "Lean for the Curious Mathematician conference", 2024, with tutorial and demo confe.
- From functional analysis to functional programming, and back , Invited talk given at the Journées Nationales du Gdr-IM in Paris in April 2023.
- Computing Analysis through Logic , Invited tutorial to the workshop on Tangent Category and Applications, BIRS, Calgary, June 2021
[video].
- Computing Analysis through Logic , a poster prepared for prize-giving ceremony L'Oréal Unesco 2019.
- Differential Linear Logic , Doctoral course on the semantics of linear logic, Copenhagen, February 2016.
- Linearity and Differentiation,PhD' Student' Semainar, LIAFA and PPS, Paris, November 2013
- Logique Linéaire et Analyse fonctionnelle, 13th forum for young mathematicians, Lyon, November 2013.
Dialectica and Automatic Differentiation
- ∂ is for Dialectica , Contributed talk at LICS, July 2024
- ∂ is for Dialectica , Invited talk to the PhilMaths Seminar, March 2024
- ∂ is for Dialectica , Invited talk to a special session on proof theory at CIE, July 2023
- ∂ is for Dialectica , Talk for Thomas Ehrhard 60's birhday, October 2023
- ∂ is for Dialectica , Invited talk to Wollic 2022, September 2022
- ∂ is for Dialectica , SEMINÁRIO DE LÓGICA MATEMÁTICA, Lisboa, Online, March 2022.
- ∂ is for Dialectica , Invited talk to the Chocola Seminar, Lyon, March 2022.
- ∂ is for Dialectica , Mathematical Foundations Seminar, Bath, Online, November 2021.
- ∂ is for Dialectica , TLLA 2021, Online Workshop, Invited Talk, June 2021.
- Typing differentiable programming , LoVe Team Seminar, LIPN, April 2021.
- Typing differentiable programming , Cosynus Team Seminar, LiX, Palaiseau, February 2020.
Distributions in Linear Logic, polarized models
- Differential Linear Logic extended to differential operators , Invited short talk to the Linear Logic Winter Schoool, CIRM, Marseille, January 2022.
- Higher-Order Distributions for Linear Logic , Invited talk to the Chocola Seminar , Lyon, November 2019.
- Higher-Order Distributions for Linear Logic , Contributed talk to FoSSacs 2019, Prague, April 2019.
- Differentiating proofs and programs , Invited talk at SYCO3, March 2019.
- A logical account for LPDEs , Higher Order Models of Differential Linear Logic, given at Bellairs Workshop in March 2019.
- A logical account for LPDEs , Seminar given at the LIX, Polytechnique, November 2018.
- A logical account for LPDEs , Contributed talk to LICS 2018, Oxford, JuLy 2018.
- A logic for LPDEs , Invited talk to a special session, Conference MFPS 2018, Halifax, Canada, June 2018.
- A Type Theory for Linear Partial Differential Equations , Poster for the Annual days of the GDR-IM, Ecole Polytechnique, April 2018.
- A Type Theory for Linear Partial Differential Equations, Antique team, ENS Ulm, Paris, March 2018.
- Smooth models of linear logic and Partial Differential Equations , Journées GEOCAL-LAC, Nantes, November 2017.
- Smooth models of linear logic and Partial Differential Equations , Seminar of the team LCR, LIPN Université Paris 13, November 2017.
- Smooth differential linear logic and Partial differentials equations , Trends in Linear Logic and Applications, Oxford, September 2017.
- Smooth models of Linear Logic : Towards a Type Theory for Linear Partial Differential Equations , Seminar Chocola, Lyon 2017, June.
- Towards a Type Theory for Linear Partial Differential Equations , PLS group, ITU Copenhagen, June 2017.
Models of LL based on the Schwartz epsilon product
- Models of LL based on the Schwartz epsilon product , Contributed talk to TLLA 2018, Oxford, JuLy 2018.
- Models of LL based on the epsilon product, an introduction to LL , joint work with Y. Dabrowski, séminaire de géométrie et physique mathématique, Paris Diderot, May 2018.
- Smooth models of linear logic , Seminar of the LIMD team, LAMA, Université Savoie Mont Blanc, Chambéry, December 2017.
- Smooth models of linear logic , Forum des jeunes mathématicien.ne.s, Nancy, 2017.
- Smooth models of Linear Logic based on the Schwartz' epsilon product , Second General Meeting of the GDRI-LL , Roma, October 2017.
- Smooth models of Differential Linear Logic , DIKU, Copenhagen, June 2017.